X:es_realizer{i:l}, P:(ES{i}Prop{i'}).
R-Feasible{i:l}(X)  (es:ES{i}. Consistent(X;es)  P(es))  es-real{i:l}(es.P(es)) 

latex

Definitions	t  T, P  Q, x:A. B(x), f(a), x(s), Consistent(R;es), Type, Prop, x:AB(x), ES, R-Feasible(R), x:AB(x), P & Q, x:A. B(x), R ||- es.P(es), es.P(es), Realizer
Lemmas	es realizer wf, R-Feasible wf, event system wf, R-consistent wf